declare OPCONST outcome(PROGRAM,STATE) = STATE;

axiom progsem:
	∀ s eta.(null(s) ⊃ outcome(s,eta)=eta),
	∀ s eta.(isli(s) ⊃ outcome(s,eta) = a(ac,arg(s),eta)),
	∀ s eta.(isload(s) ⊃ outcome(s,eta) = a(ac,cc(arg(s),eta),eta)),
	∀ s eta.(issto(s) ⊃ outcome(s,eta) = a(arg(s),cc(ac,eta),eta)),
	∀ s eta.(isadd(s) ⊃ 
		outcome(s,eta) = a(ac,plus(cc(arg(s),eta),cc(ac,eta)),eta)),
	∀ s eta.(¬null(s)∧¬null(rest(s)) ⊃
		outcome(s,eta) = outcome(rest(s),outcome(first(s),eta)));;

declare OPCONST compile(EXPRESSION,NUMBER) = PROGRAM;

declare OPCONST map(EXPRESSION) = NUMBER;

axiom compile:
	∀e t.(isconst(e) ⊃ compile(e,t) = mkli(val(e))),
	∀e t.(isvar(e) ⊃ compile(e,t) = mkload(map(e))),
	∀e t.(issum(e) ⊃ compile(e,t) = append(compile(s1(e),t),
		append(mksto(t),append(compile(e,t+1),mkadd(t)))));;

declare OPCONST load(SOURCESTATE) = STATE;

axiom map:
	∀e xi.(isvar(e) ⊃ cc(map(e),load(xi)) = c(e,xi));;

declare INDCONST t0 ε NUMBER;

axiom t0:
	ac < t0,
	∀e.map(e) < t0;;

axiom arith:
	∀x.x < x+1,
	∀x y.(x<y ⊃ ¬(x=y)),
	∀x y z.(x<y ∧ y<z ⊃ x<z);;